w:World, t:, l:IdLnk, i:Id. ||onlnk(l;m(i;t))||   

latex

Definitions	World, t  T, , IdLnk, Id, m(i;t), onlnk(l;mss), ||as||, x:A. B(x), w.M, mlnk(m), Msg, source(l), S  T, Msg(M), P  Q
Lemmas	w-m wf, Msg wf, w-M wf, length wf1, w-Msg wf, w-onlnk wf, lsrc wf, mlnk wf, Id wf, IdLnk wf, nat wf, world wf